
[POSCO.REC]
[compile a Post system into REC]
[18 December 1980]

[variable bracketed by constants, followed by another variable]
{
    [cr, lf]			(2573TL;)&
    [read console]		(R13%='';T08%(=2080[sp,bs]TL)(@J|;L@J;);)J
    [logon message]		(''TL@&'Initial Axiom:'TL@&@JI;:)R
    [to shorten program]	(UQzml;)U
    [write workspace]		(JZqt;)W
    [to shorten program]	(zZQml;)Z
    [signoff message]		(@&'Theorem:'TL@&JZqt;)X
				(@R(@&@WRL
JZ''E'!'@U0$S('!'E'['@U1$S('['E']'@U2$S(']'E'['@U3$S('['E'.'@U4$S('.'E'!'@U5$S('!'E@Z6$S(
	JZD''I0$ryGI'{`'I1$ryGI'`E`'I3$ryGI'`UQzml'I2$ryGI'$S!'I3$ryGI'['I4$ryGI'.'I5$ryGI'!nL;nL}'I6$ryGI''I;)nL;nL)nL;nL)nL;nL)nL;nL)nL;nL)nL;nL)nL:
[terminal variable]
JZ''E'!'@U0$S('!'E'['@U1$S('['E'].'@U2$S('].'E'!'@U5$S('!'E@Z6$S(
	JZD''I0$ryGI'{`'I1$ryGI'`FzZQml'I2$ryGI'$S!.'I5$ryGI'!nL;nL}'I6$ryGI''I;)nL;nL)nL;nL)nL;nL)nL;nL)nL:
[final variable, but still followed by a constant]
JZ''E'!'@U0$S('!'E'['@U1$S('['E']'@U2$S(']'E'.'@U3$S('.'E'!'@U5$S('!'E@Z6$S(
	JZD''I0$ryGI'{`'I1$ryGI'`E`'I3$ryGI'`UQzml'I2$ryGI'$S!.'I5$ryGI'!nL;nL}'I6$ryGI''I;)nL;nL)nL;nL)nL;nL)nL;nL)nL;nL)nL:
[compile the consequent]
JZ''E'#'@U0$S('#'E'['@U1$S('['E']'@U2$S(']'E'!'@U5$S('!'E@Z6$S(
	JZD''I0$ryGI'`'I1$ryGI'`I'I2$ryGI'$ryGI#'I5$ryGI'!'I6$ryGI''I;)nL;nL)nL;nL)nL;nL)nL;nL)nL:
[compile final constant in the consequent]
JZ''E'#'@U0$S('#'E'!'@U1$S('!'E@Z6$S(
	JZD''I0$ryGI'`'I1$ryGI'`I'I6$ryGI':'I;)nL;nL)nL;nL)nL:
[antecedent compiled, set up consequent]
JZ''E'!.'@U0$S('!.'E@Z6$S(
	JZD''I0$ryGI'JZD#'I6$ryGI''I;)nL;nL)nL:;)@X;)}

